0 CpxTRS
↳1 TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxWeightedTrs
↳3 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxTypedWeightedTrs
↳5 CompletionProof (UPPER BOUND(ID), 0 ms)
↳6 CpxTypedWeightedCompleteTrs
↳7 NarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
↳8 CpxTypedWeightedCompleteTrs
↳9 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 0 ms)
↳10 CpxRNTS
↳11 InliningProof (UPPER BOUND(ID), 115 ms)
↳12 CpxRNTS
↳13 SimplificationProof (BOTH BOUNDS(ID, ID), 0 ms)
↳14 CpxRNTS
↳15 CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID), 0 ms)
↳16 CpxRNTS
↳17 IntTrsBoundProof (UPPER BOUND(ID), 238 ms)
↳18 CpxRNTS
↳19 IntTrsBoundProof (UPPER BOUND(ID), 8 ms)
↳20 CpxRNTS
↳21 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳22 CpxRNTS
↳23 IntTrsBoundProof (UPPER BOUND(ID), 438 ms)
↳24 CpxRNTS
↳25 IntTrsBoundProof (UPPER BOUND(ID), 122 ms)
↳26 CpxRNTS
↳27 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳28 CpxRNTS
↳29 IntTrsBoundProof (UPPER BOUND(ID), 931 ms)
↳30 CpxRNTS
↳31 IntTrsBoundProof (UPPER BOUND(ID), 398 ms)
↳32 CpxRNTS
↳33 FinalProof (⇔, 0 ms)
↳34 BOUNDS(1, n^1)
a__f(0) → cons(0, f(s(0)))
a__f(s(0)) → a__f(a__p(s(0)))
a__p(s(0)) → 0
mark(f(X)) → a__f(mark(X))
mark(p(X)) → a__p(mark(X))
mark(0) → 0
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(s(X)) → s(mark(X))
a__f(X) → f(X)
a__p(X) → p(X)
a__f(0) → cons(0, f(s(0))) [1]
a__f(s(0)) → a__f(a__p(s(0))) [1]
a__p(s(0)) → 0 [1]
mark(f(X)) → a__f(mark(X)) [1]
mark(p(X)) → a__p(mark(X)) [1]
mark(0) → 0 [1]
mark(cons(X1, X2)) → cons(mark(X1), X2) [1]
mark(s(X)) → s(mark(X)) [1]
a__f(X) → f(X) [1]
a__p(X) → p(X) [1]
a__f(0) → cons(0, f(s(0))) [1]
a__f(s(0)) → a__f(a__p(s(0))) [1]
a__p(s(0)) → 0 [1]
mark(f(X)) → a__f(mark(X)) [1]
mark(p(X)) → a__p(mark(X)) [1]
mark(0) → 0 [1]
mark(cons(X1, X2)) → cons(mark(X1), X2) [1]
mark(s(X)) → s(mark(X)) [1]
a__f(X) → f(X) [1]
a__p(X) → p(X) [1]
a__f :: 0:s:f:cons:p → 0:s:f:cons:p 0 :: 0:s:f:cons:p cons :: 0:s:f:cons:p → 0:s:f:cons:p → 0:s:f:cons:p f :: 0:s:f:cons:p → 0:s:f:cons:p s :: 0:s:f:cons:p → 0:s:f:cons:p a__p :: 0:s:f:cons:p → 0:s:f:cons:p mark :: 0:s:f:cons:p → 0:s:f:cons:p p :: 0:s:f:cons:p → 0:s:f:cons:p |
(a) The obligation is a constructor system where every type has a constant constructor,
(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:
none
(c) The following functions are completely defined:
a__p
mark
a__f
Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
0 => 0
a__f(z) -{ 2 }→ a__f(0) :|: z = 1 + 0
a__f(z) -{ 2 }→ a__f(1 + (1 + 0)) :|: z = 1 + 0
a__f(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
a__f(z) -{ 1 }→ 1 + 0 + (1 + (1 + 0)) :|: z = 0
a__p(z) -{ 1 }→ 0 :|: z = 1 + 0
a__p(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
mark(z) -{ 2 }→ a__p(a__p(mark(X5))) :|: X5 >= 0, z = 1 + (1 + X5)
mark(z) -{ 2 }→ a__p(a__f(mark(X4))) :|: z = 1 + (1 + X4), X4 >= 0
mark(z) -{ 2 }→ a__p(0) :|: z = 1 + 0
mark(z) -{ 2 }→ a__p(1 + mark(X6)) :|: X6 >= 0, z = 1 + (1 + X6)
mark(z) -{ 2 }→ a__p(1 + mark(X1'') + X2'') :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
mark(z) -{ 2 }→ a__f(a__p(mark(X''))) :|: z = 1 + (1 + X''), X'' >= 0
mark(z) -{ 2 }→ a__f(a__f(mark(X'))) :|: X' >= 0, z = 1 + (1 + X')
mark(z) -{ 2 }→ a__f(0) :|: z = 1 + 0
mark(z) -{ 2 }→ a__f(1 + mark(X3)) :|: z = 1 + (1 + X3), X3 >= 0
mark(z) -{ 2 }→ a__f(1 + mark(X1') + X2') :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
mark(z) -{ 1 }→ 0 :|: z = 0
mark(z) -{ 1 }→ 1 + mark(X) :|: z = 1 + X, X >= 0
mark(z) -{ 1 }→ 1 + mark(X1) + X2 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
a__p(z) -{ 1 }→ 0 :|: z = 1 + 0
a__p(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
a__f(z) -{ 2 }→ a__f(0) :|: z = 1 + 0
a__f(z) -{ 2 }→ a__f(1 + (1 + 0)) :|: z = 1 + 0
a__f(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
a__f(z) -{ 1 }→ 1 + 0 + (1 + (1 + 0)) :|: z = 0
a__p(z) -{ 1 }→ 0 :|: z = 1 + 0
a__p(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
mark(z) -{ 2 }→ a__p(a__p(mark(X5))) :|: X5 >= 0, z = 1 + (1 + X5)
mark(z) -{ 2 }→ a__p(a__f(mark(X4))) :|: z = 1 + (1 + X4), X4 >= 0
mark(z) -{ 2 }→ a__p(1 + mark(X6)) :|: X6 >= 0, z = 1 + (1 + X6)
mark(z) -{ 2 }→ a__p(1 + mark(X1'') + X2'') :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
mark(z) -{ 2 }→ a__f(a__p(mark(X''))) :|: z = 1 + (1 + X''), X'' >= 0
mark(z) -{ 2 }→ a__f(a__f(mark(X'))) :|: X' >= 0, z = 1 + (1 + X')
mark(z) -{ 2 }→ a__f(0) :|: z = 1 + 0
mark(z) -{ 2 }→ a__f(1 + mark(X3)) :|: z = 1 + (1 + X3), X3 >= 0
mark(z) -{ 2 }→ a__f(1 + mark(X1') + X2') :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
mark(z) -{ 1 }→ 0 :|: z = 0
mark(z) -{ 3 }→ 1 + X :|: z = 1 + 0, X >= 0, 0 = X
mark(z) -{ 1 }→ 1 + mark(X) :|: z = 1 + X, X >= 0
mark(z) -{ 1 }→ 1 + mark(X1) + X2 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
a__f(z) -{ 2 }→ a__f(0) :|: z = 1 + 0
a__f(z) -{ 2 }→ a__f(1 + (1 + 0)) :|: z = 1 + 0
a__f(z) -{ 1 }→ 1 + z :|: z >= 0
a__f(z) -{ 1 }→ 1 + 0 + (1 + (1 + 0)) :|: z = 0
a__p(z) -{ 1 }→ 0 :|: z = 1 + 0
a__p(z) -{ 1 }→ 1 + z :|: z >= 0
mark(z) -{ 2 }→ a__p(a__p(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__p(a__f(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__p(1 + mark(z - 2)) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__p(1 + mark(X1'') + X2'') :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
mark(z) -{ 2 }→ a__f(a__p(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__f(a__f(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__f(0) :|: z = 1 + 0
mark(z) -{ 2 }→ a__f(1 + mark(z - 2)) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__f(1 + mark(X1') + X2') :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
mark(z) -{ 1 }→ 0 :|: z = 0
mark(z) -{ 3 }→ 1 + X :|: z = 1 + 0, X >= 0, 0 = X
mark(z) -{ 1 }→ 1 + mark(z - 1) :|: z - 1 >= 0
mark(z) -{ 1 }→ 1 + mark(X1) + X2 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
{ a__p } { a__f } { mark } |
a__f(z) -{ 2 }→ a__f(0) :|: z = 1 + 0
a__f(z) -{ 2 }→ a__f(1 + (1 + 0)) :|: z = 1 + 0
a__f(z) -{ 1 }→ 1 + z :|: z >= 0
a__f(z) -{ 1 }→ 1 + 0 + (1 + (1 + 0)) :|: z = 0
a__p(z) -{ 1 }→ 0 :|: z = 1 + 0
a__p(z) -{ 1 }→ 1 + z :|: z >= 0
mark(z) -{ 2 }→ a__p(a__p(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__p(a__f(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__p(1 + mark(z - 2)) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__p(1 + mark(X1'') + X2'') :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
mark(z) -{ 2 }→ a__f(a__p(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__f(a__f(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__f(0) :|: z = 1 + 0
mark(z) -{ 2 }→ a__f(1 + mark(z - 2)) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__f(1 + mark(X1') + X2') :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
mark(z) -{ 1 }→ 0 :|: z = 0
mark(z) -{ 3 }→ 1 + X :|: z = 1 + 0, X >= 0, 0 = X
mark(z) -{ 1 }→ 1 + mark(z - 1) :|: z - 1 >= 0
mark(z) -{ 1 }→ 1 + mark(X1) + X2 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
a__f(z) -{ 2 }→ a__f(0) :|: z = 1 + 0
a__f(z) -{ 2 }→ a__f(1 + (1 + 0)) :|: z = 1 + 0
a__f(z) -{ 1 }→ 1 + z :|: z >= 0
a__f(z) -{ 1 }→ 1 + 0 + (1 + (1 + 0)) :|: z = 0
a__p(z) -{ 1 }→ 0 :|: z = 1 + 0
a__p(z) -{ 1 }→ 1 + z :|: z >= 0
mark(z) -{ 2 }→ a__p(a__p(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__p(a__f(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__p(1 + mark(z - 2)) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__p(1 + mark(X1'') + X2'') :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
mark(z) -{ 2 }→ a__f(a__p(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__f(a__f(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__f(0) :|: z = 1 + 0
mark(z) -{ 2 }→ a__f(1 + mark(z - 2)) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__f(1 + mark(X1') + X2') :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
mark(z) -{ 1 }→ 0 :|: z = 0
mark(z) -{ 3 }→ 1 + X :|: z = 1 + 0, X >= 0, 0 = X
mark(z) -{ 1 }→ 1 + mark(z - 1) :|: z - 1 >= 0
mark(z) -{ 1 }→ 1 + mark(X1) + X2 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
a__p: runtime: ?, size: O(n1) [1 + z] |
a__f(z) -{ 2 }→ a__f(0) :|: z = 1 + 0
a__f(z) -{ 2 }→ a__f(1 + (1 + 0)) :|: z = 1 + 0
a__f(z) -{ 1 }→ 1 + z :|: z >= 0
a__f(z) -{ 1 }→ 1 + 0 + (1 + (1 + 0)) :|: z = 0
a__p(z) -{ 1 }→ 0 :|: z = 1 + 0
a__p(z) -{ 1 }→ 1 + z :|: z >= 0
mark(z) -{ 2 }→ a__p(a__p(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__p(a__f(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__p(1 + mark(z - 2)) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__p(1 + mark(X1'') + X2'') :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
mark(z) -{ 2 }→ a__f(a__p(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__f(a__f(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__f(0) :|: z = 1 + 0
mark(z) -{ 2 }→ a__f(1 + mark(z - 2)) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__f(1 + mark(X1') + X2') :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
mark(z) -{ 1 }→ 0 :|: z = 0
mark(z) -{ 3 }→ 1 + X :|: z = 1 + 0, X >= 0, 0 = X
mark(z) -{ 1 }→ 1 + mark(z - 1) :|: z - 1 >= 0
mark(z) -{ 1 }→ 1 + mark(X1) + X2 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
a__p: runtime: O(1) [1], size: O(n1) [1 + z] |
a__f(z) -{ 2 }→ a__f(0) :|: z = 1 + 0
a__f(z) -{ 2 }→ a__f(1 + (1 + 0)) :|: z = 1 + 0
a__f(z) -{ 1 }→ 1 + z :|: z >= 0
a__f(z) -{ 1 }→ 1 + 0 + (1 + (1 + 0)) :|: z = 0
a__p(z) -{ 1 }→ 0 :|: z = 1 + 0
a__p(z) -{ 1 }→ 1 + z :|: z >= 0
mark(z) -{ 2 }→ a__p(a__p(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__p(a__f(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__p(1 + mark(z - 2)) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__p(1 + mark(X1'') + X2'') :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
mark(z) -{ 2 }→ a__f(a__p(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__f(a__f(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__f(0) :|: z = 1 + 0
mark(z) -{ 2 }→ a__f(1 + mark(z - 2)) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__f(1 + mark(X1') + X2') :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
mark(z) -{ 1 }→ 0 :|: z = 0
mark(z) -{ 3 }→ 1 + X :|: z = 1 + 0, X >= 0, 0 = X
mark(z) -{ 1 }→ 1 + mark(z - 1) :|: z - 1 >= 0
mark(z) -{ 1 }→ 1 + mark(X1) + X2 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
a__p: runtime: O(1) [1], size: O(n1) [1 + z] |
a__f(z) -{ 2 }→ a__f(0) :|: z = 1 + 0
a__f(z) -{ 2 }→ a__f(1 + (1 + 0)) :|: z = 1 + 0
a__f(z) -{ 1 }→ 1 + z :|: z >= 0
a__f(z) -{ 1 }→ 1 + 0 + (1 + (1 + 0)) :|: z = 0
a__p(z) -{ 1 }→ 0 :|: z = 1 + 0
a__p(z) -{ 1 }→ 1 + z :|: z >= 0
mark(z) -{ 2 }→ a__p(a__p(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__p(a__f(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__p(1 + mark(z - 2)) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__p(1 + mark(X1'') + X2'') :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
mark(z) -{ 2 }→ a__f(a__p(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__f(a__f(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__f(0) :|: z = 1 + 0
mark(z) -{ 2 }→ a__f(1 + mark(z - 2)) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__f(1 + mark(X1') + X2') :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
mark(z) -{ 1 }→ 0 :|: z = 0
mark(z) -{ 3 }→ 1 + X :|: z = 1 + 0, X >= 0, 0 = X
mark(z) -{ 1 }→ 1 + mark(z - 1) :|: z - 1 >= 0
mark(z) -{ 1 }→ 1 + mark(X1) + X2 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
a__p: runtime: O(1) [1], size: O(n1) [1 + z] a__f: runtime: ?, size: O(n1) [3 + z] |
a__f(z) -{ 2 }→ a__f(0) :|: z = 1 + 0
a__f(z) -{ 2 }→ a__f(1 + (1 + 0)) :|: z = 1 + 0
a__f(z) -{ 1 }→ 1 + z :|: z >= 0
a__f(z) -{ 1 }→ 1 + 0 + (1 + (1 + 0)) :|: z = 0
a__p(z) -{ 1 }→ 0 :|: z = 1 + 0
a__p(z) -{ 1 }→ 1 + z :|: z >= 0
mark(z) -{ 2 }→ a__p(a__p(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__p(a__f(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__p(1 + mark(z - 2)) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__p(1 + mark(X1'') + X2'') :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
mark(z) -{ 2 }→ a__f(a__p(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__f(a__f(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__f(0) :|: z = 1 + 0
mark(z) -{ 2 }→ a__f(1 + mark(z - 2)) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__f(1 + mark(X1') + X2') :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
mark(z) -{ 1 }→ 0 :|: z = 0
mark(z) -{ 3 }→ 1 + X :|: z = 1 + 0, X >= 0, 0 = X
mark(z) -{ 1 }→ 1 + mark(z - 1) :|: z - 1 >= 0
mark(z) -{ 1 }→ 1 + mark(X1) + X2 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
a__p: runtime: O(1) [1], size: O(n1) [1 + z] a__f: runtime: O(1) [3], size: O(n1) [3 + z] |
a__f(z) -{ 5 }→ s :|: s >= 0, s <= 1 * 0 + 3, z = 1 + 0
a__f(z) -{ 5 }→ s' :|: s' >= 0, s' <= 1 * (1 + (1 + 0)) + 3, z = 1 + 0
a__f(z) -{ 1 }→ 1 + z :|: z >= 0
a__f(z) -{ 1 }→ 1 + 0 + (1 + (1 + 0)) :|: z = 0
a__p(z) -{ 1 }→ 0 :|: z = 1 + 0
a__p(z) -{ 1 }→ 1 + z :|: z >= 0
mark(z) -{ 5 }→ s'' :|: s'' >= 0, s'' <= 1 * 0 + 3, z = 1 + 0
mark(z) -{ 2 }→ a__p(a__p(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__p(a__f(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__p(1 + mark(z - 2)) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__p(1 + mark(X1'') + X2'') :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
mark(z) -{ 2 }→ a__f(a__p(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__f(a__f(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__f(1 + mark(z - 2)) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__f(1 + mark(X1') + X2') :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
mark(z) -{ 1 }→ 0 :|: z = 0
mark(z) -{ 3 }→ 1 + X :|: z = 1 + 0, X >= 0, 0 = X
mark(z) -{ 1 }→ 1 + mark(z - 1) :|: z - 1 >= 0
mark(z) -{ 1 }→ 1 + mark(X1) + X2 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
a__p: runtime: O(1) [1], size: O(n1) [1 + z] a__f: runtime: O(1) [3], size: O(n1) [3 + z] |
a__f(z) -{ 5 }→ s :|: s >= 0, s <= 1 * 0 + 3, z = 1 + 0
a__f(z) -{ 5 }→ s' :|: s' >= 0, s' <= 1 * (1 + (1 + 0)) + 3, z = 1 + 0
a__f(z) -{ 1 }→ 1 + z :|: z >= 0
a__f(z) -{ 1 }→ 1 + 0 + (1 + (1 + 0)) :|: z = 0
a__p(z) -{ 1 }→ 0 :|: z = 1 + 0
a__p(z) -{ 1 }→ 1 + z :|: z >= 0
mark(z) -{ 5 }→ s'' :|: s'' >= 0, s'' <= 1 * 0 + 3, z = 1 + 0
mark(z) -{ 2 }→ a__p(a__p(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__p(a__f(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__p(1 + mark(z - 2)) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__p(1 + mark(X1'') + X2'') :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
mark(z) -{ 2 }→ a__f(a__p(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__f(a__f(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__f(1 + mark(z - 2)) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__f(1 + mark(X1') + X2') :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
mark(z) -{ 1 }→ 0 :|: z = 0
mark(z) -{ 3 }→ 1 + X :|: z = 1 + 0, X >= 0, 0 = X
mark(z) -{ 1 }→ 1 + mark(z - 1) :|: z - 1 >= 0
mark(z) -{ 1 }→ 1 + mark(X1) + X2 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
a__p: runtime: O(1) [1], size: O(n1) [1 + z] a__f: runtime: O(1) [3], size: O(n1) [3 + z] mark: runtime: ?, size: O(n1) [3·z] |
a__f(z) -{ 5 }→ s :|: s >= 0, s <= 1 * 0 + 3, z = 1 + 0
a__f(z) -{ 5 }→ s' :|: s' >= 0, s' <= 1 * (1 + (1 + 0)) + 3, z = 1 + 0
a__f(z) -{ 1 }→ 1 + z :|: z >= 0
a__f(z) -{ 1 }→ 1 + 0 + (1 + (1 + 0)) :|: z = 0
a__p(z) -{ 1 }→ 0 :|: z = 1 + 0
a__p(z) -{ 1 }→ 1 + z :|: z >= 0
mark(z) -{ 5 }→ s'' :|: s'' >= 0, s'' <= 1 * 0 + 3, z = 1 + 0
mark(z) -{ 2 }→ a__p(a__p(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__p(a__f(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__p(1 + mark(z - 2)) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__p(1 + mark(X1'') + X2'') :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
mark(z) -{ 2 }→ a__f(a__p(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__f(a__f(mark(z - 2))) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__f(1 + mark(z - 2)) :|: z - 2 >= 0
mark(z) -{ 2 }→ a__f(1 + mark(X1') + X2') :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
mark(z) -{ 1 }→ 0 :|: z = 0
mark(z) -{ 3 }→ 1 + X :|: z = 1 + 0, X >= 0, 0 = X
mark(z) -{ 1 }→ 1 + mark(z - 1) :|: z - 1 >= 0
mark(z) -{ 1 }→ 1 + mark(X1) + X2 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
a__p: runtime: O(1) [1], size: O(n1) [1 + z] a__f: runtime: O(1) [3], size: O(n1) [3 + z] mark: runtime: O(n1) [9 + 36·z], size: O(n1) [3·z] |